A:MsgA. A ||+  

latex

Definitions	t  T, x:A. B(x), MsgA, ma-frame-compatible(A;B), M1 || M2, P & Q, A ||+ B
Lemmas	msga wf, ma-empty-frame-compatible-right, ma-empty-compatible-right